\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), ${\it del}$:rationals.
\\[0ex]qless(0; ${\it del}$)
\\[0ex]$\Rightarrow$ fischer\=\{\=x:ut2,\+\+
\\[0ex]try:ut2,
\\[0ex]taken:ut2,
\\[0ex]contending:ut2,
\\[0ex]free:ut2,
\\[0ex]mine:ut2,
\\[0ex]wanted:ut2,
\\[0ex]z:ut2\}
\-\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\Rightarrow$ fischer{-}delay\=\{\=i:l,\+\+
\\[0ex]x:ut2,
\\[0ex]try:ut2,
\\[0ex]taken:ut2,
\\[0ex]contending:ut2,
\\[0ex]free:ut2,
\\[0ex]mine:ut2,
\\[0ex]wanted:ut2,
\\[0ex]z:ut2\}
\-\\[0ex](${\it es}$; ${\it del}$; $L$)
\-\\[0ex]$\Rightarrow$ \=($\forall$$e$,${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]f{-}msg\=\{wanted:ut2, free:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-\\[0ex]$\Rightarrow$ f{-}msg\=\{wanted:ut2, free:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$; ${\it e'}$)
\-\\[0ex]$\Rightarrow$ (es{-}sender(${\it es}$; ${\it e'}$) = es{-}sender(${\it es}$; $e$) $\in$ es{-}E(${\it es}$))
\\[0ex]$\Rightarrow$ qless(es{-}time(${\it es}$; ${\it e'}$); (es{-}time(${\it es}$; $e$) + ${\it del}$)))
\-
\end{tabbing}